#include <string.h>
#include <stdlib.h>
#include <stdio.h>
#include <pthread.h>
#include <sched.h>
#include <time.h>
#include "solver.h"
#include "fsio.h"
#include "mem.h"

extern int nb_threads_dispo;
extern int mode_afficher_clauses;
t_litteral* solution = NULL;
pthread_mutex_t thread_lck, data_lck;
int fin = 0;

void init_threading()
{
	pthread_mutex_init(&thread_lck, NULL);
	pthread_mutex_init(&data_lck, NULL);
}

int affecter (t_matrice* matrice,
			 t_clause* tab_clauses,
			 t_litteral* tab_variables,
			 int num_var_courante)
{
	/**
	  * Le signe de num_var_courante donne le signe à affecter 
	  * à la variable. Sa valeur absolue donne le numéro
	  * de la variable.
	  **/
	if (num_var_courante < 0)
	{
		tab_variables[abs(num_var_courante)].etat = FAUX;		
	} else {
		tab_variables[abs(num_var_courante)].etat = VRAI;
	}
	
	/* Calculer l'impact sur les clauses */
	if (simplifier(matrice, tab_clauses, tab_variables, num_var_courante) < 0)
	{
		/* Un conflit a été détecté. L'affectation n'est pas possible :-( */
		return -1;
	}
	
	/* Variable affectée, problème simplifié. */
	return 1;
}

int traiter_litteraux_propres (t_matrice* matrice,
				t_clause* tab_clauses,
				t_litteral* tab_variables
				)
{
	int i, propre_existe, res = 1;
	do
	{
		propre_existe = 0;
		for (i = 1; i <= nombre_variables(tab_variables) && res; i++)
		{
			if (tab_variables[i].etat == NEUTRE)
			{
				if (tab_variables[i].nb_occ_pos == 0 && tab_variables[i].nb_occ_neg != 0)
				{
					/**
					  * Le nombre d'occurences positifs est nul, la variable prendra donc
					  * obligatoirement une valeur négative. On vérifie également si
					  * le nombre d'occurences négatives est non nul car on veut éviter
					  * d'affecter des valeurs aux variables qui ne sont pas représentées
					  * dans le problème.
					  **/
					res = affecter(matrice, tab_clauses, tab_variables, -i);
					
					/**
					  * On a trouvé un littéral propre, il en reste peut-être 
					  * d'autres. On doit réitérer encore une fois.
					  **/
					propre_existe = 1;
				} else {
					if (tab_variables[i].nb_occ_neg == 0 && tab_variables[i].nb_occ_pos != 0)
					/**
					  * Le nombre d'occurences négatives est nul, la variable prendra donc
					  * obligatoirement une valeur positives (voir plus haut).
					  */
					{
						res = affecter(matrice, tab_clauses, tab_variables, i);
						
						/**
						  * On a trouvé un littéral propre, il en reste peut-être 
						  * d'autres. On doit réitérer encore une fois.
						  **/
						propre_existe = 1;
					}
				}
			}
		}
	/**
	  * On continue tant qu'il reste des littéraux propres et 
	  * qu'on ait pas trouvé un conflit.
	  **/
	} while (propre_existe && res); 
	
	return res;
}

int traiter_clauses_unitaires (t_matrice* matrice,
			    t_clause* tab_clauses,
			    t_litteral* tab_variables)
{
	int i, num_var_courante, unitaire_existe;
	t_etat_variable etat_var_courante;
	
	do
	{
		i = 1; unitaire_existe = 0;
		
		/* Trouver la première clause unitaire. */
		while (i < nombre_clauses(tab_clauses) &&
			   (!est_unitaire(tab_clauses, i) || 
				est_marque_satisfaite(tab_clauses, i)
			   )
			  )
		{
			i++;
		}
		/** 
		  * i est l'indice de la première clause unitaire 
		  * ou la dernière clause de la matrice
		  **/
		
		if (est_unitaire(tab_clauses, i) && !est_marque_satisfaite(tab_clauses, i))
		{
			unitaire_existe = 1;
			
			/**
			  * Affecter la bonne valeur a la première clause unitaire non satisfaite.
			  * Si le signe de la variable est négatif, on lui affecte une valeur 
			  * négative...
			  */
			if (matrice->elements[tab_clauses[i].ptr_premier].num_variable < 0)
			{
				etat_var_courante = FAUX;
				
			} else {
				etat_var_courante = VRAI;
			}
			tab_variables[abs(matrice->elements[tab_clauses[i].ptr_premier].num_variable)].etat = etat_var_courante;
			num_var_courante = matrice->elements[tab_clauses[i].ptr_premier].num_variable;
		
			/* Simplifier le problème en considérant l'affectation précédente. */
			if (simplifier(matrice, tab_clauses, tab_variables, num_var_courante) < 0)
			{
				/* Conflit detecté, affectation impossible. */
				return -1;
			}
		}
	} while (unitaire_existe); /* Il existe des clauses unitaires non satisfaites. */

	/* Traitement terminé, il ne reste plus aucune clause unitaire. */	
	return 1;
}

void decr_compteur_occ (t_litteral* tab_variables, int num_var)
{
	int abs_num_var = abs(num_var); /* Numéro de la variable */
	if (num_var >= 0)
	{
		tab_variables[abs_num_var].nb_occ_pos--;
	} else {
		tab_variables[abs_num_var].nb_occ_neg--;
	}
}

void mettre_a_jour_compteurs_occ (t_matrice* matrice,
			   t_clause* tab_clauses,
			   t_litteral* tab_variables,
			   int num_clause)
{
	/* Parcourir la clause */
	t_ptr_elem courant = tab_clauses[num_clause].ptr_premier;

	while (courant != NON_SIGNIFICATIF)
	{
		decr_compteur_occ(tab_variables, matrice->elements[courant].num_variable);
		courant = matrice->elements[courant].ptr_clause_suiv;
	}
}

int simplifier (t_matrice* matrice,
			   t_clause* tab_clauses,
			   t_litteral* tab_variables,
			   int num_var_courante)
{
	int num_clause, val;
	t_ptr_elem courant_variable, courant_clause, preced_clause;

	/* On commence à la première occurence de la variable */
	courant_variable = tab_variables[abs(num_var_courante)].ptr_premier;
	
	/* Parcours dans le sens des variables */
	while (courant_variable != NON_SIGNIFICATIF)
	{
		/* Detérminer le numéro de la clause */
		num_clause = matrice->elements[courant_variable].num_clause;
		
		/* Déterminer le début de la clause */
		courant_clause = tab_clauses[num_clause].ptr_premier;
		
		/* Déterminer la valeur de la variable analysée */
		val = matrice->elements[courant_variable].num_variable;

		if (tab_clauses[num_clause].etat != SATISFAITE)
		{
			/* On ne traite que les clauses non satisfaites */
			if (num_var_courante == val)
			{
				/**
				  * La variable est du même signe que la valeur affectée,
				  * marquer la clause satisfaite
				  **/
				tab_clauses[num_clause].etat = SATISFAITE;
				(matrice->nb_clauses_a_traiter)--;
				
				/** 
				  * On peut s'arrêter tout de suite si toutes les clauses sont déjà
				  * satisfaites. On a trouvé un modèle.
				  **/
				if (matrice->nb_clauses_a_traiter == 0) { return 1; }
				
				mettre_a_jour_compteurs_occ(matrice, tab_clauses, tab_variables, num_clause);
				
			} else {
				
				/* num_var_courante = -val, il faut raccourcir la clause */
				if (matrice->elements[tab_clauses[num_clause].ptr_premier].ptr_clause_suiv == NON_SIGNIFICATIF)
				{
					/* Clause vide, nous devons revenir en arrière */
					return -1;
				}
				
				tab_clauses[num_clause].etat = RACCOURCIE;
				
				if (tab_clauses[num_clause].ptr_premier == courant_variable)
				{
					/* Le littéral à supprimer se trouve au début de la clause */
					tab_clauses[num_clause].ptr_premier = matrice->elements[courant_clause].ptr_clause_suiv;
				} else {
					/* Le littéral à supprimer se trouve au milieu de la clause */
					preced_clause = matrice->elements[courant_variable].ptr_clause_prec;
					matrice->elements[preced_clause].ptr_clause_suiv = 
						matrice->elements[courant_variable].ptr_clause_suiv;
						
					if (matrice->elements[preced_clause].ptr_clause_suiv == NON_SIGNIFICATIF)
					{
						/* Le littéral à supprimer est le dernier de la clause */
						tab_clauses[num_clause].ptr_dernier = preced_clause;
					} else {
						matrice->elements[matrice->elements[courant_variable].ptr_clause_suiv].ptr_clause_prec =
							preced_clause;
					}
				}
			}
		}
		/* Passer à l'occurence suivante de la variable */
		courant_variable = matrice->elements[courant_variable].ptr_var_suiv;
	}

	/* Simplification terminée mais nous n'avons pas encore résolu le problème */
	return 0;
}
		
int choisir_var (t_litteral* tab_variables)
{
	int i = 1, max;

// Le choix aléatoire s'est avéré inefficace	
//	/* Essayons d'abord une affectation aleatoire */
//	if (rand() % 100 < 20)
//	{
//		i = rand() % tab_variables[0].nombre + 1;
//		//printf("i=%d\n", i);
//		if (tab_variables[i].etat == NEUTRE)
//		{
//			return (tab_variables[i].nb_occ_pos > tab_variables[i].nb_occ_neg) ? i : -i;
//		}
//		i = 1;
//	}
//	/* La variable a déjà été affectée, passons à l'algorithme de choix d'une variable classique */

	/* Déterminer la variable avec le plus d'occurences */
	while (i <= nombre_variables(tab_variables) && tab_variables[i].etat != NEUTRE) i++;
	if (i <= nombre_variables(tab_variables) && tab_variables[i].etat == NEUTRE)
	{
		max = i;
		for (i = max+1; i<=nombre_variables(tab_variables); i++)
		{
			if (tab_variables[i].etat == NEUTRE && 
				((tab_variables[max].nb_occ_pos + tab_variables[max].nb_occ_neg) <
				 (tab_variables[i].nb_occ_pos + tab_variables[i].nb_occ_neg))
				)
			{
				max = i;
			}
		}
		
		/**
		  * Si la variable a plus d'occurences négatives que positives, on retourne
		  * l'opposé de la variable pour signaler à la fonction d'affectation qu'elle
		  * doit affecter une valeur négative à la variable.
		  */
		return (tab_variables[max].nb_occ_pos > tab_variables[max].nb_occ_neg) ? max : -max;

	} else {
		return 0; /* Toutes les variables ont déjà été affectées */
	}
}
	
int resoudre (t_matrice* matrice,
			  t_clause* tab_clauses,
			  t_litteral* tab_variables,
			  int niv)
{
	
	int res1, res2; /* Résultats des threads */
	int thread = 0; /* Vrai si une séparation de threads a été effectuée */
	int nb_clauses_a_traiter;
	pthread_t thr1, thr2;

	int taille_tab_variables = (tab_variables[0].ptr_premier + 1) * sizeof(t_litteral);
	int taille_tab_clauses = (tab_clauses[0].ptr_premier + 1) * sizeof(t_clause);
	
	t_litteral* nouv_tab_variables = allouer(taille_tab_variables, VARIABLES);
	t_clause* nouv_tab_clauses = allouer(taille_tab_clauses, CLAUSES);
	t_matrice nouv_matrice =
		{ .elements = allouer(matrice->taille * sizeof(t_element), ELEMENTS),
		  .nb_elements = matrice->nb_elements,
		  .taille = matrice->taille
	    };

	t_litteral* nouv_tab_variables_2;
	t_clause* nouv_tab_clauses_2;
	t_matrice nouv_matrice_2;

	tester_param_t tester_param =
		{ .matrice = matrice,
		  .tab_clauses = tab_clauses,
		  .tab_variables = tab_variables,
		  .niv = niv,
		  .nouv_tab_variables = nouv_tab_variables,
		  .nouv_tab_clauses = nouv_tab_clauses,
		  .nouv_matrice = &nouv_matrice,
		  .thread = 0,
		};
	
	//printf("Niveau : %d\n", niv);
	
	/* Traiter les clauses unitaires */
	if (traiter_clauses_unitaires(matrice, tab_clauses, tab_variables) < 0)
	{
		/* Conflit détecté */
		restituer_tout(nouv_matrice.elements, nouv_tab_clauses, nouv_tab_variables);
		return -1;
	}
	traiter_litteraux_propres(matrice, tab_clauses, tab_variables);	

	if (mode_afficher_clauses)
	{
		if (niv == 0)
		{
			/* Afficher les clauses après la première simplification */
			afficher_clauses(matrice, tab_clauses); printf("\n\n");
		}
	}
	
	/**
	  * Sauver le nombre de clauses qui ne sont pas satisfaites, 
	  * on en aura besoin si la première affectation
	  * ne marche pas.
	  **/
	nb_clauses_a_traiter = matrice->nb_clauses_a_traiter;
	nouv_matrice.nb_clauses_a_traiter = nb_clauses_a_traiter;

	if (toutes_satisfaites(matrice))
	{
		/* Toutes les clauses ont été satisfaites, on arrête. */
		if (solution == NULL)
		{
			/* Copier le modèle trouvé dans une zone mémoire spécifique. */
			solution = allouer(taille_tab_variables, VARIABLES);
			memcpy(solution, tab_variables, taille_tab_variables);
		}
	 	restituer_tout(nouv_matrice.elements, nouv_tab_clauses, nouv_tab_variables);
		
		return 1;
	}

	/* Choisir la variable à affecter */
	tester_param.variable_choisie = choisir_var(tab_variables);

	/* Il ne reste plus aucune variable à affecter */
	if (tester_param.variable_choisie == 0)
	{
		restituer_tout(nouv_matrice.elements, nouv_tab_clauses, nouv_tab_variables);
		return toutes_satisfaites(matrice);
	}

	pthread_mutex_lock(&thread_lck);

	if (nb_threads_dispo >= 2)
	{
		nb_threads_dispo -= 2;

		nouv_tab_variables_2 = allouer(taille_tab_variables, VARIABLES);
		nouv_tab_clauses_2 = allouer(taille_tab_clauses, CLAUSES);
		nouv_matrice_2.elements = allouer(matrice->taille * sizeof(t_element), ELEMENTS);
		nouv_matrice_2.nb_elements = matrice->nb_elements;
		nouv_matrice_2.taille = matrice->taille;
		nouv_matrice_2.nb_clauses_a_traiter = nb_clauses_a_traiter;
		    
		tester_param_t tester_param_2 =
			{ .matrice = matrice,
			  .tab_clauses = tab_clauses,
			  .tab_variables = tab_variables,
			  .niv = niv,
			  .nouv_tab_variables = nouv_tab_variables_2,
			  .nouv_tab_clauses = nouv_tab_clauses_2,
			  .nouv_matrice = &nouv_matrice_2,
			  .variable_choisie = tester_param.variable_choisie,
			  .thread = 1
			};
		
		tester_param.thread = 1;
		
		pthread_create(&thr1, NULL, (void*)tester, &tester_param);
		pthread_create(&thr2, NULL, (void*)tester, &tester_param_2);
		thread = 1;
		
	}
	pthread_mutex_unlock(&thread_lck);
	
	if (thread)
	{
		pthread_join(thr1, (void*)&res1);
		if (res1 == 1)
		{
			/* Toutes les clauses sont satisfaites */
			restituer_tout(nouv_matrice.elements, nouv_tab_clauses, nouv_tab_variables);
			fin = 1;
			return 1;
		} else {
			pthread_join(thr2, (void*)&res2);
			restituer_tout(nouv_matrice_2.elements, nouv_tab_clauses_2, nouv_tab_variables_2);

			if (res2 == 1)
			{
				/* Toutes les clauses sont satisfaites */
				restituer_tout(nouv_matrice.elements, nouv_tab_clauses, nouv_tab_variables);
				fin = 1;
				return 1;
			}
		}

	} else {
		/* Traitement sans threads */
		if (tester(&tester_param) == 1)
		{
			/* Toutes les clauses sont satisfaites */
			restituer_tout(nouv_matrice.elements, nouv_tab_clauses, nouv_tab_variables);
			fin = 1;
			return 1;
		}
		
		nouv_matrice.nb_clauses_a_traiter = nb_clauses_a_traiter;
		tester_param.variable_choisie *= -1;
		
		if (tester(&tester_param) == 1)
		{
			/* Toutes les clauses sont satisfaites */
			restituer_tout(nouv_matrice.elements, nouv_tab_clauses, nouv_tab_variables);
			fin = 1;
			return 1;
		}			
	}

	restituer_tout(nouv_matrice.elements, nouv_tab_clauses, nouv_tab_variables);
	return -1;
}


int tester (tester_param_t* tester_param)
{
	int taille_tab_variables = (tester_param->tab_variables[0].ptr_premier + 1) * sizeof(t_litteral);
	int taille_tab_clauses = (tester_param->tab_clauses[0].ptr_premier + 1) * sizeof(t_clause);
	int thread = tester_param->thread;
	
	
	tester_param->thread = 0;


	if (fin)
	{
		/* Court-circuit multithreading (l'autre thread a déjà trouvé une solution) */
		if (thread)
		{
			pthread_exit((void*) -2);
		} else {
			return -2;
		}
	}

	/* Dupliquer les clauses originales */
	memcpy(tester_param->nouv_tab_variables, tester_param->tab_variables, taille_tab_variables);
	memcpy(tester_param->nouv_tab_clauses, tester_param->tab_clauses, taille_tab_clauses);
	memcpy(tester_param->nouv_matrice->elements, tester_param->matrice->elements, tester_param->matrice->taille * sizeof(t_element)); 
	
	/* Affecter la valeur à la variable choisie */
	if (affecter(tester_param->nouv_matrice, tester_param->nouv_tab_clauses, tester_param->nouv_tab_variables, tester_param->variable_choisie) < 0)
	{
		if (thread)
		{
			pthread_mutex_lock(&thread_lck);
			nb_threads_dispo++;
			pthread_mutex_unlock(&thread_lck);
			pthread_exit((void*) -1);
		} else {
			return -1;
		}
	}


	if ((toutes_satisfaites(tester_param->nouv_matrice)) ||
		(resoudre(tester_param->nouv_matrice, 
				  tester_param->nouv_tab_clauses,
				  tester_param->nouv_tab_variables,
				  tester_param->niv+1)
				  	== 1)
	   ) // Il reste des clauses non satisfaites
	{
		
		if (solution == NULL)
		{
			solution = allouer(taille_tab_variables, VARIABLES);
			memcpy(solution, tester_param->nouv_tab_variables, taille_tab_variables);
		}
		
		if (thread)
		{
			pthread_mutex_lock(&thread_lck);
			nb_threads_dispo++;
			pthread_mutex_unlock(&thread_lck);
			pthread_exit((void*) 1);
		} else {
			return 1;
		}
	}

	if (thread)
	{
		pthread_mutex_lock(&thread_lck);
		nb_threads_dispo++;
		pthread_mutex_unlock(&thread_lck);
		pthread_exit((void*) -1);
	} else {
		return -1;
	}
}
